x, y:Atom. x =a y   

latex

Up	bool 1, bool 1
Definitions	x =a y, t  T, x:A. B(x), A, P  Q, False
Lemmas	bfalse wf, btrue wf